In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of the canonical axiomatic set theory ZFC. A statement in the language of ZFC is provable in NBG if and only if it is provable in ZFC. The ontology of NBG includes proper classes, objects having members but that cannot be members of other entities. NBG's principle of class comprehension is predicative; quantified variables in the defining formula can range only over sets. Allowing impredicative comprehension turns NBG into Morse-Kelley set theory (MK). NBG, unlike ZFC and MK, can be finitely axiomatized.
Contents |
The defining aspect of NBG is the distinction between proper class and set. Let a and s be two individuals. Then the atomic sentence is defined if a is a set and s is a class. In other words, is defined unless a is a proper class. A proper class is very large; NBG even admits of "the class of all sets", the universal class called V. However, NBG does not admit "the class of all classes" (which fails because proper classes are not "objects" that can be put into classes in NBG) or "the set of all sets" (whose existence cannot be justified with NBG axioms).
By NBG's axiom schema of Class Comprehension, all objects satisfying any given formula in the first order language of NBG form a class; if the class would not be a set in ZFC, it is an NBG proper class.
The development of classes mirrors the development of naive set theory. The principle of abstraction is given, and thus classes can be formed out of all individuals satisfying any statement of first order logic whose atomic sentences all involve either the membership relation or predicates definable from membership. Equality, pairing, subclass, and such, are all definable and so need not be axiomatized — their definitions denote a particular abstraction of a formula.
Sets are developed in a manner very similarly to ZF. Let Rp(A,a), meaning "the set a represents the class A," denote a binary relation defined as follows:
That is, a "represents" A if every element of a is an element of A, and conversely. Classes lacking representations, such as the class of all sets that do not contain themselves (the class invoked by the Russell paradox), are the proper classes.
The first variant of NBG, by John von Neumann in the 1920s, took functions and not sets, as primitive. In a series of articles published 1937-54, Paul Bernays modified Von Neumann's theory so as to make sets and set membership primitive; he also discovered that it could be finitely axiomatized. Gödel (1940), while investigating the independence of the Continuum hypothesis, further simplified and used the theory. Montague (1961) showed that ZFC cannot be finitely axiomatized.
NBG is presented here as a two-sorted theory, with lower case letters denoting variables ranging over sets, and upper case letters denoting variables ranging over classes. Hence "" should be read "set x is a member of set y," and "" as "set x is a member of class Y." Statements of equality may take the form "" or "". "" stands for "" and is an abuse of notation. NBG can also be presented as a one-sorted theory of classes, with sets being those classes that are members of at least one other class.
We first axiomatize NBG using the axiom schema of Class Comprehension. This schema is provably equivalent[1] to 9 of its finite instances, stated in the following section. Hence these 9 finite axioms can replace Class Comprehension. This is the precise sense in which NBG can be finitely axiomatized.
The following five axioms are identical to their ZFC counterparts:
The remaining axioms have capitalized names because they are primarily concerned with classes rather than sets. The next two axioms differ from their ZFC counterparts only in that their quantified variables range over classes, not sets:
The last two axioms are peculiar to NBG:
An appealing but somewhat mysterious feature of NBG is that its axiom schema of Class Comprehension is equivalent to the conjunction of a finite number of its instances. The axioms of this section may replace the Axiom Schema of Class Comprehension in the preceding section. The finite axiomatization presented below does not necessarily resemble exactly any NBG axiomatization in print.
We develop our axiomatization by considering the structure of formulas.
This axiom, in combination with the set existence axioms from the previous axiomatization, assures the existence of classes from the outset, and enables formulas with class parameters.
Let and Then and suffice for handling all sentential connectives, because ∧ and ¬ are a functionally complete set of connectives.
We now turn to quantification. In order to handle multiple variables, we need the ability to represent relations. Define the ordered pair as as usual. Note that three applications of pairing to a and b assure that (a,b) is indeed a set.
These axioms license adding dummy arguments, and rearranging the order of arguments, in relations of any arity. The peculiar form of Association is designed exactly to make it possible to bring any term in a list of arguments to the front (with the help of Converses). We represent the argument list as (it is a pair with the first argument as its first projection and the "tail" of the argument list as the second projection). The idea is to apply Assoc1 until the argument to be brought to the front is second, then apply Conv1 or Conv2 as appropriate to bring the second argument to the front, then apply Assoc2 until the effects of the original applications of Assoc1 (which are now behind the moved argument) are corrected.
If is a class considered as a relation, then its range, is a class. This gives us the existential quantifier. The universal quantifier can be defined in terms of the existential quantifier and negation.
The above axioms can reorder the arguments of any relation so as to bring any desired argument to the front of the argument list, where it can be quantified.
Finally, each atomic formula implies the existence of a corresponding class relation:
Diagonal, together with addition of dummy arguments and rearrangement of arguments, can build a relation asserting the equality of any two of its arguments; thus repeated variables can be handled.
Mendelson (1997: 230) refers to his axioms B1-B7 of class comprehension as "axioms of class existence." Four of these identical to axioms already stated above: B1 is Membership; B2, Intersection; B3, Complement; B5, Product. B4 is Ranges modified to assert the existence of the domain of R (by existentially quantifying y instead of x). The last two axioms are:
B6 and B7 enable what Converses and Association enable: given any class X of ordered triples, there exists another class Y whose members are the members of X each reordered in the same way.
For a discussion of some ontological and other philosophical issues posed by NBG, especially when contrasted with ZFC and MK, see Appendix C of Potter (2004).
Even though NBG is a conservative extension of ZFC, a theorem may have a shorter and more elegant proof in NBG than in ZFC (or vice versa). For a survey of known results of this nature, see Pudlak (1998).
ZFC, NBG, and MK have models describable in terms of V, the standard model of ZFC and the von Neumann universe. Now let the members of V include the inaccessible cardinal κ. Also let Def(X) denote the Δ0 definable subsets of X (see constructible universe). Then:
The ontology of NBG provides scaffolding for speaking about "large objects" without risking paradox. In some developments of category theory, for instance, a "large category" is defined as one whose objects make up a proper class, with the same being true of its morphisms. A "small category", on the other hand, is one whose objects and morphisms are members of some set. We can thus easily speak of the "category of all sets" or "category of all small categories" without risking paradox. Those categories are large, of course. There is no "category of all categories" since it would have to contain the category of small categories, although yet another ontological extension can enable one to talk formally about such a "category" (see for example the "quasicategory of all categories" of Adámek et al. (1990), whose objects and morphisms form a "proper conglomerate").
On whether an ontology including classes as well as sets is adequate for category theory, see Muller (2001).